Nuprl Definition : p-lift
11,40
postcript
pdf
p-lift(
d
;
f
)(
x
) == case
d
(
x
) of inl(
a
) => inl (
f
(
x
)) | inr(
a
) => inr
a
latex
Definitions
x
.
A
(
x
)
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
inl
x
,
f
(
a
)
,
inr
x
FDL editor aliases
p-lift
origin
x.A(x)x.A(x)